package flowlogic;

import ast.ChannelConstant;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;

import util.Pair;

import ast.Constant;
import ast.CstPr;
import ast.Endorse;
import ast.Function;
import ast.Label;
import ast.Principal;
import ast.Site;
import ast.Term;
import ast.TermVar;

public class ConstraintSolver {
	
	private HashMap<String, HashSet<Term>> rho;
	private HashMap<String, HashSet<Term>> kappa;
	
	public ConstraintSolver(
			HashMap<String, HashSet<Term>> r, 
			HashMap<String, HashSet<Term>> k)
	{
		rho = r;
		kappa = k;
	}

	// return true if "constraint" holds before this operation
	
	public boolean solve(Constraint constraint)
	{
		HashMap<String, Term> inst = new HashMap<String, Term>();
		return solveConstraint(inst, constraint);
	}
	
	public boolean solveConstraint(HashMap<String, Term> inst, Constraint constraint)
	{
		boolean holds = true;
		
		if (constraint instanceof GuardedConstraint) {
			
			if (solveConstraint(inst, ((GuardedConstraint) constraint).getGuard()) == true) {
				holds = solveConstraint(inst, 
						((GuardedConstraint) constraint).getConstraint());
			} 
			
		} else if (constraint instanceof ForallConstraint) {
			
			HashMap<String, Term> ist = new HashMap<String, Term>();
			ist.putAll(inst);
			String bvName = ((ForallConstraint) constraint).getBv().getName();
			HashSet<Term> terms = ((ForallConstraint) constraint).getRange().getTerms();
			for (Term t : terms) {
				ist.put(bvName, t);
				boolean hld = solveConstraint(ist, ((ForallConstraint) constraint).getBody());
				ist.remove(bvName);
				
				if (!hld)
					holds = false;
			}
			
		} else if (constraint instanceof Negation) {
			
			Constraint inner = ((Negation) constraint).getNegatedConstraint();
			holds = !solveConstraint(inst, inner);
			
		} else if (constraint instanceof Inclusion) {
			
			Node leftNode = ((Inclusion) constraint).getLeft();
			Node rightNode = ((Inclusion) constraint).getRight();
			Object o1 = solveNode(inst, leftNode);
			Object o2 = solveNode(inst, rightNode);
			holds = checkAndMakeInclusion(o1, o2, ((Inclusion) constraint).getAct());
			
		} else if (constraint instanceof ExtNode) {
			
			Node innerRes = ((ExtNode) constraint).getOfNode();
			Object o = solveNode(inst, innerRes);
			assert (o instanceof ChannelConstant);
			holds = ((ChannelConstant) o).getLabel().isExternal();
			
		} else if (constraint instanceof IntNode) {
			
			Node innerRes = ((IntNode) constraint).getOfNode();
			Object o = solveNode(inst, innerRes);
			assert (o instanceof ChannelConstant);
			holds = !((ChannelConstant) o).getLabel().isExternal();
			
		} 
		
		return holds;
	}
	
	private Object solveNode(HashMap<String, Term> inst, Node node) 
	{
		Object result = null;
		
		if (node instanceof TpNode) {
			
			Node inner = ((TpNode) node).getOfNode();
			Object innerRes = solveNode(inst, inner);
			if (innerRes instanceof TermVar) {
				if (STSimplifier.getChannelMap().containsKey(((TermVar) innerRes).getName())) {
					result = ChannelTp.getInstance();
				} else if (STSimplifier.getSites().contains(((TermVar) innerRes).getName())) {
					result = SiteTp.getInstance();
				} else if (STSimplifier.getPrincipals().contains(((TermVar) innerRes).getName())) {
					result = PrincipalTp.getInstance();
				}
			} else if (innerRes instanceof ExternalData) {
				result = DataTp.getInstance();
			}
			
		} else if (node instanceof FunNode) {
			
			String textRes = "";
			
			ArrayList<FreeVariable> argList = ((FunNode) node).getArgList();
			Function func = ((FunNode) node).getFunction();
			ArrayList<String> argumentValues = new ArrayList<String>();
			for (FreeVariable arg : argList) {
				Term mapsTo = (Term) solveNode(inst, arg);
				assert(mapsTo instanceof CstPr);
				if (mapsTo instanceof Constant) { 
					argumentValues.add(((Constant) mapsTo).getName());
				} else if (mapsTo instanceof Principal) {
					argumentValues.add(((Principal) mapsTo).getName());
				}
			}
			
			if (argumentValues.contains("#d")) {
				result = ExternalData.getInstance();
			} else {
				for (Pair<ArrayList<String>, String> row : func.getDefinition())
				{
					if (argumentValues.equals(row.getFst())) {
						textRes = row.getSnd();
						break;
					}
				}
			}
			
			if (STSimplifier.getChannelMap().containsKey(textRes)) {
				result = STSimplifier.getChannelMap().get(textRes);
			} else if (STSimplifier.getSites().contains(textRes)) {
				result = new Site(textRes);
			} else if (STSimplifier.getPrincipals().contains(textRes)) {
				result = new Principal(textRes);
			}
			
		} else if (node instanceof ConcreteSetNode) {
			
			HashSet<Node> innerSet = ((ConcreteSetNode) node).getSet();
			boolean ofNodes = false;
			for (Node n : innerSet) {
				if (n instanceof SignalValue || n instanceof TpValue ||
					n instanceof TpNode) 
				{
					ofNodes = true;
					break;
				}
			}
			
			if (ofNodes) {
				result = new HashSet<Node>();
				for (Node n : innerSet) {
					((HashSet<Node>) result).add((Node) solveNode(inst, n));
				}
			} else {
				result = new HashSet<Term>();
				for (Node n : innerSet) {
					((HashSet<Term>) result).add((Term) solveNode(inst, n));
				}
			}
			
		} else if (node instanceof ResNode) {
			
			result = ((ResNode) node).getTerms();
		
		} else if (node instanceof PsiNode) { 
		
			result = ((PsiNode) node).getErrs();
			
		} else if (node instanceof RhoNode) {
			
			Node inner = ((RhoNode) node).getOfNode();
			assert (inner instanceof FreeVariable);
			String name = ((FreeVariable) inner).getName();
			if (!rho.containsKey(name)) {
				rho.put(name, new HashSet<Term>());
			}
			result = rho.get(name);
			
		} else if (node instanceof KappaNode) {
			
			Node inner = ((KappaNode) node).getOfNode();
			Object o = solveNode(inst, inner);
			assert (o instanceof Constant);
			String name = ((Constant) o).getName();
			if (!kappa.containsKey(name)) {
				kappa.put(name, new HashSet<Term>());
			}
			result = kappa.get(name);
			
		} else if (node instanceof FreeVariable) {
			
			String fvName = ((FreeVariable) node).getName();
			assert (inst.containsKey(fvName));
			result = inst.get(fvName);
			
		} else if (node instanceof TpValue) {
			
			result = node;
			
		} else if (node instanceof SignalValue) {
			
			result = node;
		}
	    
		return result;
	}
	
	private static int numOfConstraints = 0;
	
	private boolean checkAndMakeInclusion(Object o1, Object o2, boolean act)
	{
		boolean res = false;
		HashSet s1 = (HashSet) o1;
		HashSet s2 = (HashSet) o2;
		
//		try {
		if (s2.containsAll(s1)) {
			res = true;
		} else {
			if (act)
				((HashSet) o2).addAll(s1);
		}
//		} catch (NullPointerException e) {
//			System.out.println(o1);
//			System.out.println(o2);
//			System.exit(1);
//		}
		
		return res;
	}
	

}
